﻿using System;
using System.Collections.Generic;
using System.Collections;
using System.Text;
using System.Windows.Forms;

namespace mi2project
{
    //Leítram , hogy hogyan kellene műküdnie , egyenlőre még nem jól működik
    //A kirajzolás biztosan nem jó,az EsVagyFa repr.-ban váltottam Hashtable-ra
    //Arra kérnélek titeket,hogy nézzétek meg,hátha találtok benne hibát
    //A szétválasztás sem biztos,hogy jó, ill az összefűzés
    //Példa3-ra igazat kellene adnia,Példa4-re hamisat, de most mindegyikre igazat ad
    //valószínű azért mert a lepes()-ben először megvizsgálja,hogy üres-e a verem
    //és ott igazra állítja a sikerességet
    //de üres verem csak sikeres illesztések estetén alakulhatna ki 


    public enum BizonyitasTipusa2 { elore, vissza }

    public struct Ax_Par
    {
        public Axioma ax1;
        public Axioma ax2;
        public Ax_Par(Axioma Ax1, Axioma Ax2)
        {
            ax1 = Ax1;
            ax2 = Ax2;
        }
    }

    //Működése a köv lenne: a szabaly_tabla-ban (Hashtable) eltárolom a szabályokat (sorszám,axióma-pár) formájában
    //sorszámozás 1-től történik a szabályok számáig
    //a csucs_szabály(Hashtable) egy int-pár, az első int a csúcs sorszáma, a 2.-ik a szabály sorszáma
    // visszalépésnél ezt használom,hogy az adott sorszámú csúcshoz melyik sorszámú szabály volt utoljára alkalmazva
    //és a köv. sorszámúnál folytatom próbát
    //az akt_csucsok egy verem, ahhoz kell , hogy egyrészt tárolja,hogy melyik sorszámú csúcsokra kell még illeszteni
    //másrészt egy sorrendet ad,hiszen azzal hogy a tetejéről veszek ki egy sorszámot,mindig a legbaloldalibb csúcs
    //sorszmáma(amire illeszteni kell) lesz a tetjén
    //
    class VisszalepesesKereses2
    {
        public VisszalepesesKereses2(BizonyitasTipusa2 tipus, int me)
        {
            melyseg = me;
            irany = tipus;
            csucs_sorszam = 1;
            alg_vege = false;
            sikeres = false;
            myfa = new EsVagyFa2();
            tenyek = new List<Axioma>();
            szabalyok = new List<Axioma>();
            celok = new List<Axioma>();
            csucs_szabaly = new Hashtable();
            szabaly_tabla = new Hashtable();
            akt_csucsok = new Stack<int>();

        }

        //az Osszefuzest átírtam,mert az Axiomák közé nem tett operátort,csak simán összecsatolta a listákat
        //de ottvan amit te írtál kommentben, szerintem szükség lenne az utolso operator elvételére
        //ezért odatettem egy utolsoOperatortElvesz() fv.-t
        //Startcsucs sorszáma 1, az ő szülőé pedig -1
        public void start(SzabalyalapuReprezentacio sz_r)
        {
            this.repr = sz_r;
            tenyek = sz_r.getTenyek();
            szabalyok = sz_r.getSzabalyok();
            celok = sz_r.getCelok();


            Axioma teljes;//= new Axioma();
            if (irany == BizonyitasTipusa2.elore)
            {
                //teljes = Osszefuz(tenyek);
                Osszefuz(tenyek, out teljes);
                myfa.startCsucsBeszurasa(1, teljes);
                /*foreach (Axioma teny in sz_r.getTenyek())
                    teljes.hozzafuz(teny, "&");

                teljes.utolsoOperatortElvesz();
                myfa.startCsucsBeszurasa(1, teljes);*/
            }
            else
            {
                //teljes = Osszefuz(celok);
                Osszefuz(celok, out teljes);
                myfa.startCsucsBeszurasa(1, teljes);
                /*foreach (Axioma teny in sz_r.getTenyek())
                    teljes.hozzafuz(teny, "&");

                teljes.utolsoOperatortElvesz();
                myfa.startCsucsBeszurasa(1, teljes);*/
            }

            Szabaly_tabla_kitoltes();
            csucs_szabaly.Add(1, 0);//a 0 azt jelenti,hogy még nem illesztettem szabályt
            akt_csucsok.Push(1);
            csucs_sorszam++;
        }

        //akkor van vége az algoritmusnak, amikor kiürül a verem(vagyis nincs mire illeszteni)
        //ilyenkor sikeresen ér véget az algoritmus
        //illetve akkor van vége , ha startcsucsból akarunk visszalépni(ilyenkor sikertelen)
        //egy lépés abból áll,hogy kiveszem a verem tetején lévő elemet(int),ez a sorszáma annak a csucsnak
        //amire illeszteni kell, ha nem literál,akkor szétbontom és a 2 gyereket beilllesztema fába
        //ha ezen sorszámú csúcsban lévő axióma egy literált tartalmaz akkor
        //először az iránytól függően tényt vagy célt próbálok illeszeni
        //ha nem lehet,akkor szabályt illesztek
        //ha nem illeszthető szabály , akkor visszalépés következik erre a csúcsra
        //a visszalépés fv-nél leírom,hogy hogyan működik

        public void lepes()
        {
            if (akt_csucsok.Count == 0)
            {
                alg_vege = true;
                sikeres = true;
                return;
            }

            if (alg_vege)
            {
                return;
            }

            int vizsgalando = akt_csucsok.Pop();//kiveszem a veremből azt a sorszámot , amire illeszteni kell
            //ha sikerül tényt vagy célt illeszteni,akkor a semmit nem teszek vissza a verembe a helyére
            //ha szabályt illesztek akkor a szabály megfelelő oldalán(imp.előtt vagy után) álló axiómát
            //egy csúcsba teszem megsorszámozva és a sorszáma a verembe kerül,tehát legközelebb ezt veszem ki

            if (myfa.Melyseg() >= melyseg)
            {
                Visszalepes(vizsgalando);
                return;
            }

            int hanyadik_szabaly;
            Axioma ax = new Axioma();

            if (myfa.IsLiteral(vizsgalando))
            {
                ax = myfa.getCsucsAxioma(vizsgalando);
                //string literal = ax.getLiteralok()[1].getJel();
                //bool negalas = ax.getLiteralok()[1].getNegalas();
                if (irany == BizonyitasTipusa2.elore)
                {
                    foreach (Axioma cel in celok)
                    {
                        if (ax.getLiteralok()[0].getJel() == cel.getLiteralok()[0].getJel())
                        {
                            if (ax.getLiteralok()[0].getNegalas() == cel.getLiteralok()[0].getNegalas())
                            {
                                myfa.csucsBeszuras(csucs_sorszam, vizsgalando, cel, irany);
                                csucs_sorszam++;
                                return;
                            }
                        }
                    }
                }
                else
                {
                    foreach (Axioma teny in tenyek)
                    {
                        if (ax.getLiteralok()[0].getJel() == teny.getLiteralok()[0].getJel())
                        {
                            if (ax.getLiteralok()[0].getNegalas() == teny.getLiteralok()[0].getNegalas())
                            {
                                myfa.csucsBeszuras(csucs_sorszam, vizsgalando, teny, irany);
                                csucs_sorszam++;
                                return;
                            }
                        }
                    }
                }

                if (csucs_szabaly.ContainsKey(vizsgalando))
                {
                    hanyadik_szabaly = (int)csucs_szabaly[vizsgalando];
                }
                else
                {
                    hanyadik_szabaly = 0;
                }

                int i = hanyadik_szabaly + 1;
                Axioma ax_ill = new Axioma();

                while (i <= szabaly_tabla.Count)
                {
                    if (Hasznalhato(i, vizsgalando))
                    {
                        if (irany == BizonyitasTipusa2.elore)
                        {
                            ax_ill = ((Ax_Par)szabaly_tabla[i]).ax2;
                        }
                        else
                        {
                            ax_ill = ((Ax_Par)szabaly_tabla[i]).ax1;
                        }

                        //if (Konzisztencia_ellenorzes())
                        //{
                        if (csucs_szabaly.ContainsKey(vizsgalando))
                        {
                            csucs_szabaly[vizsgalando] = i;
                        }
                        else
                        {
                            csucs_szabaly.Add(vizsgalando, i);
                        }

                        myfa.csucsBeszuras(csucs_sorszam, vizsgalando, ax_ill, irany);
                        akt_csucsok.Push(csucs_sorszam);
                        csucs_sorszam++;
                        return;

                        //}

                    }
                    i++;
                }


                Visszalepes(vizsgalando);
            }
            else  // szétválasztja a vizsgalando csúcsban lévő axiómát és beszúrja a fába a gyerekeiként
            {     //a szétválasztott axiómákat

                //Ax_Par par = new Ax_Par();
                Axioma ax1;// = new Axioma();
                Axioma ax2;// = new Axioma();

                ax = myfa.getCsucsAxioma(vizsgalando);
                //par = Szetvalaszt(ax);
                ax.szetvalasztas(out ax1, out ax2);
                int elso;

                myfa.csucsBeszuras(csucs_sorszam, vizsgalando, ax1, irany);
                //akt_csucsok.Push(csucs_sorszam);
                elso = csucs_sorszam;
                csucs_sorszam++;

                myfa.csucsBeszuras(csucs_sorszam, vizsgalando, ax2, irany);

                //Először a jobboldali gyereket teszem a verembe,de csak akkor ha a szülőből hiperél indul ki
                //az hogy a szülőből hiperél indul ki, azt jelenti hogy a másik gyerekre is illeszteni kell 
                //majd a későbbiekben,ezért kerül a jobbolali gyerek sorszáma a verembe ilyenkor
                //a baloldali gyerek sorszáma mindenképpen belekerül a verembe

                if (Hiperel(vizsgalando))
                {
                    akt_csucsok.Push(csucs_sorszam);//jobboldali gyerek sorszáma a verembe kerül
                }

                akt_csucsok.Push(elso);//baloldali gyerek sorszáma a verembe kerül
                csucs_sorszam++;
            }
        }


        public bool vege() { return alg_vege; }

        // Ha egy csúcsból hiperél indul ki,akkor mindkét gyerekre illeszteni kell majd szabályt
        //ha nem akkor csak az egyikre elegendő
        private bool Hiperel(int vizsgalando)
        {
            if (irany == BizonyitasTipusa2.elore)
            {
                if (GyerekekTipusa2.es == myfa.getCsucsGyerekeinekTipusa(vizsgalando))
                {
                    return false;
                }
                return true;
            }
            else //if(irany == BizonyitasTipusa.vissza)
            {
                if (GyerekekTipusa2.vagy == myfa.getCsucsGyerekeinekTipusa(vizsgalando))
                {
                    return false;
                }
                return true;
            }

        }

        //Visszalépés az adott sorszámú csúcsra
        //ilyenkor az adott sorszámú csúcsot mindenképp törölni kell a fából
        //de az nem lenne jó megoldás ha a szülő sorszámát visszatenném a verembe
        //a lepes() fv-ben a visszalépés a vizsgálandóra történik
        //a gyerek szülő párossal végzem a visszalépéseket
        //ezekkel határozom meg,hogy mi kerüljön a verembe,amit a köv. lépésnél majd kiveszek és arra illesztek
        //vizsgálni kell,hogyha a szülőből hiperél indul ki,akkor mindkét gyerekét törölni kell
        //hiszen ha a bal gyereket törölni kell,és a szülőből hiperél indul ki akkor a jobb gyereket már
        //nem érdemes megvizsgálni(mivel mindkét gyerekre kellett volna illeszteni)
        //ilyenkor lépünk egy szinttel feljebb,vagyis a gyerek a szülő lesz,a szülő meg az előző szülő szülője
        //ha nem hiperél indul ki és:
        //-a baloldali gyerekkel lépünk vissza:
        //  még megvizsgálható a jobboldali gyerek,ezért visszatesszük a verembe 
        //  és a visszalépés fv.véget ér(l=false)
        //-a jobboldali gyerekkel lépünk vissza:
        //ilyenkor mivel a balt már vizsgáltuk,ezért nem tesszük a verembe,hanem visszalépünk egy szintet
        //vagyis gyerek = szulo;  szulo = myfa.egyCsucsSzuloje(gyerek)
        //mindig vizsgáljuk hogy a visszalépés nem a szülőcsúcsból történt-e: if (szulo == -1)
        //ilyenkor az algoritmus véget ér sikertelenül
        //ha a szülő literál,akkor visszatehetjük őt a verembe(később egy másik szabály még illeszthető rá)

        private void Visszalepes(int elem)
        {
            int gyerek = elem;
            int szulo = myfa.egyCsucsSzuloje(elem);
            //myfa.levelCsucsTorlese(elem);
            bool l = true;
            while (l)
            {
                if (szulo == -1)
                {
                    alg_vege = true;
                    sikeres = false;
                    l = false;
                }
                else
                {

                    if (!myfa.IsLiteral(szulo))
                    {
                        if (Hiperel(szulo))
                        {
                            if (szulo == myfa.egyCsucsSzuloje(akt_csucsok.Peek()))
                            {
                                //int testver = akt_csucsok.Pop();
                                //myfa.levelCsucsTorlese(akt_csucsok.Pop());
                                akt_csucsok.Pop();
                            }

                            //akt_csucsok.Push(myfa.egyCsucsSzuloje(szulo));
                            List<int> gyerekek = myfa.egyCsucsGyerekei(szulo);
                            myfa.levelCsucsTorlese(gyerekek[0]);
                            myfa.levelCsucsTorlese(gyerekek[0]);
                            //myfa.levelCsucsTorlese(elem);
                            //myfa.levelCsucsTorlese(szulo);
                            gyerek = szulo;
                            szulo = myfa.egyCsucsSzuloje(gyerek);
                        }
                        else
                        {

                            List<int> gyerekek = myfa.egyCsucsGyerekei(szulo);
                            if (gyerek == gyerekek[0])
                            {
                                akt_csucsok.Push(gyerekek[1]);
                                l = false;
                            }
                            else
                            {
                                myfa.levelCsucsTorlese(gyerekek[0]);
                                myfa.levelCsucsTorlese(gyerekek[0]);
                                //akt_csucsok.Push(myfa.egyCsucsSzuloje(szulo));
                                //myfa.levelCsucsTorlese(szulo);
                                gyerek = szulo;
                                szulo = myfa.egyCsucsSzuloje(gyerek);

                            }

                        }
                    }
                    else
                    {
                        akt_csucsok.Push(szulo);
                        myfa.levelCsucsTorlese(gyerek);
                        l = false;
                    }
                }
            }
        }


        //az Axióma osztályban lévő operatorokhozAd fv-el nem jól műküdik,mert így duplán tesz bele az op.rangokat
        //ezért használtam a te szetvalasztas(out Axioma ax1, out Axioma ax2) fv-edet ehelyett
        private Ax_Par Szetvalaszt(Axioma vizsgalando)
        {

            Axioma ax = new Axioma();
            Axioma ax1 = new Axioma();
            Axioma ax2 = new Axioma();
            List<Literal> literalok = new List<Literal>();
            List<String> operatorok = new List<String>();
            List<Parameter> parameterek = new List<Parameter>();
            List<int> rangok = new List<int>();

            ax = vizsgalando;
            int valaszto = ax.Fo_Muv_Jel();
            int i = 1;
            int summa = 0;


            literalok = ax.getLiteralok();
            foreach (Literal l in literalok)
            {
                if (i <= valaszto)
                {
                    ax1.literalokhozAd(l);
                    summa += l.getParameterekSzama();
                }
                else
                {
                    ax2.literalokhozAd(l);
                }
                i++;
            }

            i = 1;
            operatorok = ax.getOperatorok();
            foreach (String s in operatorok)
            {
                if (i < valaszto)
                {
                    ax1.operatorokhozAd(s);
                }
                else if (i > valaszto)
                {
                    ax2.operatorokhozAd(s);
                }
                i++;
            }

            i = 1;
            rangok = ax.getOperatorokRangja();
            foreach (int r in rangok)
            {
                if (i < valaszto)
                {
                    ax1.operatorranghozAd(r);
                }
                else if (i > valaszto)
                {
                    ax2.operatorranghozAd(r);
                }
                i++;
            }

            i = 1;
            parameterek = ax.getParameterek();
            foreach (Parameter p in parameterek)
            {
                if (i <= summa)
                {
                    ax1.parameterekhezAd(p);
                }
                else
                {
                    ax2.parameterekhezAd(p);
                }
                i++;
            }

            return new Ax_Par(ax1, ax2);

        }

        //az iránynak megfelelően megnézi, hogy alkalmazható-e a szabály(int) sorszámú szabály
        //a csucs(int) sorszámú csúcsra
        private bool Hasznalhato(int szabaly, int csucs)
        {
            Axioma ax = new Axioma();
            ax = myfa.getCsucsAxioma(csucs);
            Axioma sz_ax = new Axioma();

            if (irany == BizonyitasTipusa2.elore)
            {
                sz_ax = ((Ax_Par)szabaly_tabla[szabaly]).ax1;
            }
            else
            {
                sz_ax = ((Ax_Par)szabaly_tabla[szabaly]).ax2;
            }

            if (sz_ax.getLiteralok()[0].getJel() == ax.getLiteralok()[0].getJel())
            {
                if (sz_ax.getLiteralok()[0].getNegalas() == ax.getLiteralok()[0].getNegalas())
                {
                    return true;
                }
            }
            return false;
        }

        /*private bool Konzisztencia_ellenorzes()
        {

            throw new Exception("The method or operation is not implemented.");
        }*/

        //Nem jól működött a operatorokhozAd_List miatt,mivel meghítam utána az .operatorranghozAd_List-t
        //így duplán kerültek bele a rangok, de már kikommenteztem
        //még kell majd axioma.operatorokhozAd("&", 0) , kivéve az utolsóra
        private void Osszefuz(List<Axioma> lista, out Axioma axioma)
        {
            //Axioma osszefuzott = new Axioma();
            axioma = new Axioma();
            foreach (Axioma ax in lista)
            {
                axioma.literalokhozAd_List(ax.getLiteralok());
                axioma.operatorokhozAd_List(ax.getOperatorok(), ax.getOperatorokRangja());
                axioma.parameterekhezAd_List(ax.getParameterek());
                //axioma.operatorranghozAd_List(ax.getOperatorokRangja());
                /*if (lista.IndexOf(ax) < lista.Capacity - 1)
                {
                    axioma.operatorokhozAd("&", 0);
                }*/
            }

            //return osszefuzott;
        }


        //a szabály tábla kitöltése a szetvalasztas(out ax1, out ax2)fv segítségével
        private void Szabaly_tabla_kitoltes()
        {
            Ax_Par ax_par;
            Axioma ax1;
            Axioma ax2;
            int j = 1;

            foreach (Axioma ax in szabalyok)
            {
                ax.szetvalasztas(out ax1, out ax2);

                //ax_par = Szetvalaszt(ax);
                ax_par = new Ax_Par(ax1, ax2);
                szabaly_tabla.Add(j, ax_par);
                j++;
            }
        }

        public void setMelyseg(int m)
        {
            melyseg = m;
        }

        public int getMelyseg()
        {
            return melyseg;
        }

        public void keresesVegrehajtas()
        {
            while (!vege())
            {
                //csucsnalTart = szabadLevelCsucsok.Dequeue();
                //if (bizonyitasiFa.getCsucsSorszamAlapjan(csucsnalTart).getMelyseg() < melyseg)
                lepes();
            }
        }

        public bool sikeresseg()
        {
            if (vege())
            {
                return sikeres;
            }
            else
            {
                throw new Exception("Nem ért véget az algoritmus!");
            }
        }

        //mivel átírtam az EsVagyFa-ban a fa reprezentácót Hashtable-ra(egyszerűbbnek tűnt a kezelés szempontjából)
        // így viszont nem jól működik, visszatérhetünk az előző repr-ra vagy ezt kéne kijavítani
        //a ht Hashtableban elmentem , hogy egy sorszámnak(de.Key) mi az indexe(i)
        public TreeView kirajzolas()
        {
            TreeView fa = new TreeView();
            List<TreeNode> ideglenesLista = new List<TreeNode>();
            Hashtable ht = new Hashtable();

            //int l = akt_csucsok.GetEnumerator();
            int i = 0;
            foreach (DictionaryEntry de in myfa.getCsucsok())
            {
                ideglenesLista.Add(new TreeNode(((Csucs2)de.Value).getAxioma().axiomaNezete()));
                ht.Add(de.Key, i);
                i++;
            }
            i = 0;
            foreach (DictionaryEntry de in myfa.getCsucsok())
            {

                foreach (int gyerekSzama in ((Csucs2)de.Value).getGyerekei())
                {

                    ideglenesLista[i].Nodes.Add(ideglenesLista[(int)ht[gyerekSzama]]);
                }
                i++;
            }

            fa.Nodes.Add(ideglenesLista[0]);


            return fa;


            /*
                for (int i = 0; i < myfa.csucsokSzama(); i++)
                {
                    ideglenesLista.Add(new TreeNode(myfa.getCsucsIndexAlapjan(i).getAxioma().axiomaNezete()));
                }
            for (int i = 0; i < myfa.csucsokSzama(); i++)
            {
                foreach (int gyerekSzama in myfa.getCsucsIndexAlapjan(i).getGyerekei())
                {
                    ideglenesLista[i].Nodes.Add(ideglenesLista[bizonyitasiFa.index(bizonyitasiFa.getCsucsSorszamAlapjan(gyerekSzama).getSorszam())]);
                }
            }
            fa.Nodes.Add(ideglenesLista[0]);


            return fa;*/
        }


        private SzabalyalapuReprezentacio repr;
        private EsVagyFa2 myfa;
        private int melyseg;
        int csucs_sorszam;
        private bool alg_vege, sikeres;
        private BizonyitasTipusa2 irany;
        private List<Axioma> tenyek;
        private List<Axioma> celok;
        private List<Axioma> szabalyok;
        private Hashtable csucs_szabaly;
        private Hashtable szabaly_tabla;
        private Stack<int> akt_csucsok;


    }


}
